Lambda Calculus
Table of Contents
- Equivalent to procedural computing used in turing machine. They can be translated to each other.
- It was devised by Alonzo Church
1. Church-Turing Thesis
It is philosophical argument
Turing machine and lambda calculus represents the two opposite side within the deciplines of computer science, which are bottom-up approach and top-down approach. But this thesis suggest that they are equivalent.
1.1. Statement
Lambda calculus and Turing machine is two system that describes the same fundamental nature of computation.
2. Rules
2.1. Construction
- Of Lambda Terms
- \(x\): A variables is a sequence of symbols representing a parameter.
- \((\lambda x.M)\): A lambda abstraction is a function definition that takes the bound variable \(x\) and returns \(M\).
- \((M\ N)\): An application that applies \(M\) to an argument \(N\).
2.2. Reduction
- Operations
- \((\lambda x.M[x])\to (\lambda y. M[y])\): α-conversion
- \(((\lambda x.M)\ N)\to (M[x:=N])\): β-reduction
- The result of reduction is called β-normal form.
3. Notation
- \((\lambda x.\lambda y.x + y + 1)\ 2\ 3 = 6\)
- It can be abbreviated: \(\lambda a.\lambda b.\lambda c.b = \lambda abc.b\)
4. Combinatory Logic
- The expressions in combinatory logic can be directly translated into the language of lambda calculus.
- Study of first class, higher order functions with no free variables. Study of combinators.
4.1. Combinators
- Every Program can be written in terms of S and K, Moreover, in terms of ι.
4.1.1. Definition
- Functions with no free variables.
4.1.1.1. I
- Ix = x
- λx.x
4.1.1.2. K
- Kxy = x
- λx.λy.x
4.1.1.3. N
- N := KI
- Nxy = y
- (λx.λy.x)(λz.z) = λy.λz.z
4.1.1.4. B
- Bfgx = f(gx)
4.1.1.5. C
- Cfgx = fxg
4.1.1.6. S
- Sfgx = fx(gx)
4.1.1.7. W
- Wxy = xyy
4.1.1.8. S' or Φ
- Starling' or Phoenix
- Φfghx = f(gx)(hx)
- Φ := B(BS)B
4.1.1.9. D
- Dfgxy = fx(gy)
4.1.1.10. T
- Txf = fx
- T := CI
4.1.1.11. M
- Mf = ff
- M := SII
4.1.1.12. V
- Vxyz = zxy
- V := BCT
4.1.1.13. Y
- Yf = f(Yf)
- This enables recursion.
- Y := BM(CBM)
- By Haskell Curry
- Θ := M(B(SI)M)
- By Alan Turing
- Essentials: Functional Programming's Y Combinator - Computerphile - YouTube
- λf.(λx.f(xx))(λx.f(xx))
- This is general recursion
- Self-application, the very idea of Haskell Curry
- λf.(λx.f(xx))(λx.f(xx))
4.1.1.14. Ω
- Ω = Ω
- Ω := MM
4.1.2. Extensionally Equal
- They are the same in effect.
Combinators are evaluated lazily, which means the expressions in parenthesis stay as is until it is the leading combinator and the evaluation happens from the leading one.
4.2. History
- It was developed in search of the foundation of mathematics.
- Schönfinkel
- Curry
- Church
- Turing
4.3. Church Encoding
4.3.1. Boolean
- T - True : K
- F - False : KI = CK
- NOT : C
- or NOT := C(T False) True
- AND : p => q => pqp
- OR: p => q => ppq
- BEQ: p => q => p(q)(NOT q)
4.3.2. Natural Numbers
- Pair x y := Vxy
- Pair x y True = x, Pair x y False = y
- 0 = f => a => a
- 0: I
- 1 = f => a => fa
- SUCC = n => f => a => f(nfa)
- or SUCC := Pair False
- n = SUCC n-1
- ISZERO = n => n (K False) True
- or IsZero := T True
- MULT = B
5. Currying
5.1. Definition
The natural bijection between: \[ \operatorname{curry}\colon Z^{X\times Y} \to (Z^Y)^X. \]